De Bruijn Factor

de Bruijn Factor

ド・ブラウン因子？ or ド・ブラウン係数？

形式的な数学的証明を書くことがどれだけ難しいかを示す尺度

ニコラース・ホーヴァート・ド・ブラウン(Nicolaas Govert de Bruijn)が考えたもの

詳細はPDFを見る

概要 我々は、通常の数学的説明文のサイズと、コンピュータ内部での完全な形式的翻訳との間のde Bruijnの「損失係数」を研究する。この係数は、原文に存在する詳細の量と、形式化に使用されるシステムの表現力の組み合わせによって決定される。具体的な3つの例では、この係数はおよそ4となる。